(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)
(declare-fun v5 () Real)
(declare-fun v6 () Real)
(assert (let ((e7 3))
(let ((e8 8))
(let ((e9 0))
(let ((e10 (- v0)))
(let ((e11 (- e10)))
(let ((e12 (- v0 v2)))
(let ((e13 (+ v4 e12)))
(let ((e14 (- v6 e12)))
(let ((e15 (- v2)))
(let ((e16 (* v0 v5)))
(let ((e17 (+ e14 e11)))
(let ((e18 (/ e7 (- e7))))
(let ((e19 (+ e10 e13)))
(let ((e20 (- e18 v2)))
(let ((e21 (- e14 e20)))
(let ((e22 (- v4)))
(let ((e23 (* e21 e22)))
(let ((e24 (+ e16 e20)))
(let ((e25 (+ e11 e14)))
(let ((e26 (+ e19 e16)))
(let ((e27 (+ e20 v2)))
(let ((e28 (- e22 e11)))
(let ((e29 (/ e8 (- e8))))
(let ((e30 (+ e27 e15)))
(let ((e31 (- e12)))
(let ((e32 (/ e8 (- e8))))
(let ((e33 (- v1)))
(let ((e34 (+ e26 e13)))
(let ((e35 (- e21 e28)))
(let ((e36 (/ e9 (- e7))))
(let ((e37 (- v6 e32)))
(let ((e38 (- v0)))
(let ((e39 (* e30 e23)))
(let ((e40 (- e31 e19)))
(let ((e41 (- e16 e34)))
(let ((e42 (+ e28 e20)))
(let ((e43 (* e19 e42)))
(let ((e44 (- e30)))
(let ((e45 (- e42 e14)))
(let ((e46 (+ v1 e30)))
(let ((e47 (- e18 e37)))
(let ((e48 (* (- e8) v4)))
(let ((e49 (+ e15 e46)))
(let ((e50 (- e18 e38)))
(let ((e51 (* e16 e8)))
(let ((e52 (- e21 e14)))
(let ((e53 (* e30 (- e8))))
(let ((e54 (/ e8 (- e7))))
(let ((e55 (- e31)))
(let ((e56 (- e27 e35)))
(let ((e57 (- e24 e32)))
(let ((e58 (* e23 v3)))
(let ((e59 (= v5 e58)))
(let ((e60 (distinct e20 e10)))
(let ((e61 (= e29 e23)))
(let ((e62 (< e29 e54)))
(let ((e63 (<= v1 v1)))
(let ((e64 (<= v0 v6)))
(let ((e65 (>= e23 e23)))
(let ((e66 (<= e21 e22)))
(let ((e67 (distinct e21 e16)))
(let ((e68 (>= e50 e30)))
(let ((e69 (>= e24 e17)))
(let ((e70 (< e26 e43)))
(let ((e71 (distinct e29 e40)))
(let ((e72 (distinct e13 e11)))
(let ((e73 (>= e35 e11)))
(let ((e74 (>= e15 e31)))
(let ((e75 (< e15 e48)))
(let ((e76 (<= e14 e39)))
(let ((e77 (>= e26 e26)))
(let ((e78 (distinct e38 e51)))
(let ((e79 (<= e18 v1)))
(let ((e80 (= e53 e22)))
(let ((e81 (distinct e20 e24)))
(let ((e82 (distinct e35 e19)))
(let ((e83 (= e26 e50)))
(let ((e84 (< e29 e27)))
(let ((e85 (<= v1 e13)))
(let ((e86 (> e46 e33)))
(let ((e87 (> e47 e47)))
(let ((e88 (>= v4 e16)))
(let ((e89 (distinct e54 e25)))
(let ((e90 (> e45 e28)))
(let ((e91 (distinct e14 e54)))
(let ((e92 (> e47 e22)))
(let ((e93 (< v0 v2)))
(let ((e94 (distinct v1 e12)))
(let ((e95 (< e27 e45)))
(let ((e96 (= e33 e29)))
(let ((e97 (distinct e45 e18)))
(let ((e98 (> e42 e35)))
(let ((e99 (>= e25 e42)))
(let ((e100 (> v3 e25)))
(let ((e101 (= e15 e34)))
(let ((e102 (>= e17 e43)))
(let ((e103 (<= e41 e27)))
(let ((e104 (<= e40 e55)))
(let ((e105 (<= e27 e36)))
(let ((e106 (<= e50 e31)))
(let ((e107 (<= v4 e34)))
(let ((e108 (<= e38 e27)))
(let ((e109 (> e46 e27)))
(let ((e110 (>= e11 e17)))
(let ((e111 (<= e27 e38)))
(let ((e112 (< e38 e48)))
(let ((e113 (< e41 v3)))
(let ((e114 (>= v3 e15)))
(let ((e115 (= e19 e14)))
(let ((e116 (= e22 e27)))
(let ((e117 (<= e45 e51)))
(let ((e118 (distinct v4 e25)))
(let ((e119 (> e37 e49)))
(let ((e120 (> v3 e28)))
(let ((e121 (distinct e49 e45)))
(let ((e122 (< e41 e26)))
(let ((e123 (>= e35 e25)))
(let ((e124 (> e20 e42)))
(let ((e125 (distinct v5 e13)))
(let ((e126 (> e30 e17)))
(let ((e127 (<= e41 e29)))
(let ((e128 (= e12 e10)))
(let ((e129 (> e19 e13)))
(let ((e130 (= e26 e36)))
(let ((e131 (>= e24 e44)))
(let ((e132 (distinct e44 v1)))
(let ((e133 (< e54 e32)))
(let ((e134 (distinct e43 e57)))
(let ((e135 (<= e14 e55)))
(let ((e136 (>= e17 e11)))
(let ((e137 (= e14 e38)))
(let ((e138 (= e39 v0)))
(let ((e139 (= e53 e40)))
(let ((e140 (<= e24 e47)))
(let ((e141 (< v4 v1)))
(let ((e142 (>= e42 e44)))
(let ((e143 (< e55 e54)))
(let ((e144 (>= v0 e56)))
(let ((e145 (distinct e43 e32)))
(let ((e146 (= e34 e52)))
(let ((e147 (distinct e52 e42)))
(let ((e148 (distinct e23 e49)))
(let ((e149 (> e22 e19)))
(let ((e150 (= e57 e29)))
(let ((e151 (distinct e19 e10)))
(let ((e152 (> e40 e30)))
(let ((e153 (<= e22 e24)))
(let ((e154 (< e30 e41)))
(let ((e155 (> e37 e36)))
(let ((e156 (>= e17 e52)))
(let ((e157 (= e31 e41)))
(let ((e158 (distinct e49 e26)))
(let ((e159 (>= e48 e23)))
(let ((e160 (< e34 e28)))
(let ((e161 (distinct e52 e34)))
(let ((e162 (> e57 e53)))
(let ((e163 (= e15 e28)))
(let ((e164 (>= e23 e12)))
(let ((e165 (< e10 v3)))
(let ((e166 (>= e12 e11)))
(let ((e167 (< e55 e57)))
(let ((e168 (distinct e19 e26)))
(let ((e169 (> e55 e53)))
(let ((e170 (distinct e58 e28)))
(let ((e171 (< e37 e53)))
(let ((e172 (<= e14 e54)))
(let ((e173 (> e31 e31)))
(let ((e174 (> v3 e58)))
(let ((e175 (= e52 e30)))
(let ((e176 (>= e57 e43)))
(let ((e177 (= e14 e35)))
(let ((e178 (<= e27 e22)))
(let ((e179 (>= v0 e16)))
(let ((e180 (> e12 e57)))
(let ((e181 (= e33 e57)))
(let ((e182 (distinct v4 e50)))
(let ((e183 (>= e27 e16)))
(let ((e184 (< e33 e42)))
(let ((e185 (<= e38 v4)))
(let ((e186 (distinct e23 e20)))
(let ((e187 (= e55 e54)))
(let ((e188 (distinct v5 v4)))
(let ((e189 (>= e44 e47)))
(let ((e190 (= e31 e51)))
(let ((e191 (< e53 e41)))
(let ((e192 (distinct e23 e15)))
(let ((e193 (>= e53 e54)))
(let ((e194 (< e19 v5)))
(let ((e195 (> e33 e35)))
(let ((e196 (>= e29 e43)))
(let ((e197 (distinct e23 e40)))
(let ((e198 (= e47 e27)))
(let ((e199 (< e41 e45)))
(let ((e200 (= e42 e41)))
(let ((e201 (= e34 e55)))
(let ((e202 (> e15 v5)))
(let ((e203 (> e36 e45)))
(let ((e204 (= e14 e20)))
(let ((e205 (> e52 e19)))
(let ((e206 (distinct e53 e29)))
(let ((e207 (< e20 e12)))
(let ((e208 (> e19 e28)))
(let ((e209 (> e39 e11)))
(let ((e210 (distinct e37 e50)))
(let ((e211 (>= e27 e44)))
(let ((e212 (<= v6 v4)))
(let ((e213 (> v0 e42)))
(let ((e214 (<= e46 e37)))
(let ((e215 (>= e35 e46)))
(let ((e216 (<= v3 e51)))
(let ((e217 (distinct e32 e14)))
(let ((e218 (distinct e32 e48)))
(let ((e219 (<= e37 e25)))
(let ((e220 (distinct e38 e23)))
(let ((e221 (distinct v0 e43)))
(let ((e222 (distinct e12 e32)))
(let ((e223 (> e28 e14)))
(let ((e224 (> e14 e46)))
(let ((e225 (distinct e25 e21)))
(let ((e226 (>= e21 e35)))
(let ((e227 (<= e10 e39)))
(let ((e228 (>= e40 e15)))
(let ((e229 (< e26 e18)))
(let ((e230 (>= e41 e15)))
(let ((e231 (< v6 v5)))
(let ((e232 (= v0 e12)))
(let ((e233 (>= e36 e46)))
(let ((e234 (<= e19 e26)))
(let ((e235 (<= e21 v2)))
(let ((e236 (= e58 e29)))
(let ((e237 (= e16 v6)))
(let ((e238 (< v5 e27)))
(let ((e239 (distinct e52 e27)))
(let ((e240 (< e30 e56)))
(let ((e241 (distinct e50 v1)))
(let ((e242 (distinct e53 e11)))
(let ((e243 (> v6 e51)))
(let ((e244 (> e18 e15)))
(let ((e245 (distinct v6 v6)))
(let ((e246 (= e26 e16)))
(let ((e247 (<= e29 e48)))
(let ((e248 (= e50 e39)))
(let ((e249 (>= v2 e49)))
(let ((e250 (<= e53 e48)))
(let ((e251 (= e12 e17)))
(let ((e252 (> e32 v5)))
(let ((e253 (distinct v5 v4)))
(let ((e254 (>= e45 e53)))
(let ((e255 (<= e48 e49)))
(let ((e256 (distinct v0 e22)))
(let ((e257 (distinct e21 e18)))
(let ((e258 (= e41 e18)))
(let ((e259 (= e55 v1)))
(let ((e260 (< e53 e35)))
(let ((e261 (< e13 e33)))
(let ((e262 (=> e73 e152)))
(let ((e263 (not e226)))
(let ((e264 (=> e245 e59)))
(let ((e265 (not e215)))
(let ((e266 (and e128 e229)))
(let ((e267 (and e130 e235)))
(let ((e268 (ite e122 e263 e155)))
(let ((e269 (xor e225 e92)))
(let ((e270 (= e141 e165)))
(let ((e271 (and e162 e162)))
(let ((e272 (ite e71 e93 e182)))
(let ((e273 (= e270 e83)))
(let ((e274 (=> e99 e63)))
(let ((e275 (and e232 e185)))
(let ((e276 (not e201)))
(let ((e277 (ite e190 e80 e257)))
(let ((e278 (= e68 e105)))
(let ((e279 (and e119 e179)))
(let ((e280 (xor e227 e121)))
(let ((e281 (and e89 e173)))
(let ((e282 (and e281 e137)))
(let ((e283 (= e61 e85)))
(let ((e284 (=> e278 e153)))
(let ((e285 (or e166 e248)))
(let ((e286 (and e261 e246)))
(let ((e287 (not e157)))
(let ((e288 (xor e123 e78)))
(let ((e289 (xor e82 e96)))
(let ((e290 (= e178 e111)))
(let ((e291 (xor e199 e277)))
(let ((e292 (=> e194 e113)))
(let ((e293 (or e283 e132)))
(let ((e294 (=> e191 e149)))
(let ((e295 (or e170 e125)))
(let ((e296 (or e214 e291)))
(let ((e297 (and e62 e203)))
(let ((e298 (=> e139 e176)))
(let ((e299 (and e134 e271)))
(let ((e300 (or e84 e127)))
(let ((e301 (ite e129 e163 e282)))
(let ((e302 (xor e161 e159)))
(let ((e303 (ite e267 e107 e228)))
(let ((e304 (xor e90 e143)))
(let ((e305 (not e211)))
(let ((e306 (ite e60 e167 e234)))
(let ((e307 (not e133)))
(let ((e308 (not e298)))
(let ((e309 (and e169 e230)))
(let ((e310 (ite e145 e204 e287)))
(let ((e311 (=> e100 e144)))
(let ((e312 (not e299)))
(let ((e313 (and e206 e135)))
(let ((e314 (not e216)))
(let ((e315 (ite e238 e314 e306)))
(let ((e316 (or e310 e284)))
(let ((e317 (and e251 e151)))
(let ((e318 (= e286 e142)))
(let ((e319 (not e237)))
(let ((e320 (or e231 e219)))
(let ((e321 (= e81 e213)))
(let ((e322 (ite e97 e302 e104)))
(let ((e323 (ite e290 e126 e319)))
(let ((e324 (= e180 e304)))
(let ((e325 (not e321)))
(let ((e326 (ite e131 e196 e108)))
(let ((e327 (ite e102 e110 e296)))
(let ((e328 (not e101)))
(let ((e329 (not e109)))
(let ((e330 (xor e74 e200)))
(let ((e331 (and e222 e243)))
(let ((e332 (not e164)))
(let ((e333 (=> e266 e309)))
(let ((e334 (= e318 e264)))
(let ((e335 (ite e253 e66 e255)))
(let ((e336 (xor e329 e115)))
(let ((e337 (=> e112 e87)))
(let ((e338 (ite e174 e67 e300)))
(let ((e339 (ite e307 e171 e247)))
(let ((e340 (and e106 e76)))
(let ((e341 (or e98 e315)))
(let ((e342 (=> e328 e295)))
(let ((e343 (and e64 e249)))
(let ((e344 (and e188 e341)))
(let ((e345 (ite e326 e252 e95)))
(let ((e346 (xor e239 e138)))
(let ((e347 (xor e342 e254)))
(let ((e348 (ite e88 e241 e335)))
(let ((e349 (and e289 e316)))
(let ((e350 (not e285)))
(let ((e351 (xor e320 e207)))
(let ((e352 (=> e259 e187)))
(let ((e353 (xor e317 e350)))
(let ((e354 (or e72 e184)))
(let ((e355 (not e346)))
(let ((e356 (not e330)))
(let ((e357 (= e220 e258)))
(let ((e358 (not e337)))
(let ((e359 (or e86 e91)))
(let ((e360 (ite e351 e250 e332)))
(let ((e361 (not e322)))
(let ((e362 (ite e339 e209 e352)))
(let ((e363 (or e340 e345)))
(let ((e364 (not e240)))
(let ((e365 (ite e158 e354 e146)))
(let ((e366 (=> e177 e224)))
(let ((e367 (and e244 e363)))
(let ((e368 (and e297 e262)))
(let ((e369 (ite e79 e347 e276)))
(let ((e370 (not e305)))
(let ((e371 (not e312)))
(let ((e372 (and e183 e195)))
(let ((e373 (ite e212 e210 e311)))
(let ((e374 (or e160 e75)))
(let ((e375 (=> e280 e279)))
(let ((e376 (or e192 e293)))
(let ((e377 (ite e333 e223 e154)))
(let ((e378 (not e70)))
(let ((e379 (=> e65 e202)))
(let ((e380 (or e288 e366)))
(let ((e381 (= e348 e198)))
(let ((e382 (= e181 e303)))
(let ((e383 (ite e256 e301 e69)))
(let ((e384 (xor e374 e383)))
(let ((e385 (and e116 e308)))
(let ((e386 (=> e150 e124)))
(let ((e387 (xor e385 e186)))
(let ((e388 (ite e269 e323 e189)))
(let ((e389 (= e382 e344)))
(let ((e390 (ite e217 e103 e273)))
(let ((e391 (or e377 e384)))
(let ((e392 (= e242 e338)))
(let ((e393 (= e77 e380)))
(let ((e394 (ite e357 e140 e136)))
(let ((e395 (or e389 e343)))
(let ((e396 (and e268 e359)))
(let ((e397 (xor e175 e381)))
(let ((e398 (=> e118 e156)))
(let ((e399 (and e396 e327)))
(let ((e400 (ite e233 e265 e365)))
(let ((e401 (not e193)))
(let ((e402 (xor e313 e292)))
(let ((e403 (ite e364 e358 e353)))
(let ((e404 (and e391 e386)))
(let ((e405 (= e272 e356)))
(let ((e406 (ite e336 e331 e367)))
(let ((e407 (xor e403 e168)))
(let ((e408 (xor e360 e361)))
(let ((e409 (= e197 e369)))
(let ((e410 (ite e334 e407 e387)))
(let ((e411 (and e294 e395)))
(let ((e412 (not e378)))
(let ((e413 (=> e324 e400)))
(let ((e414 (or e402 e221)))
(let ((e415 (or e409 e376)))
(let ((e416 (and e394 e260)))
(let ((e417 (or e117 e413)))
(let ((e418 (ite e147 e218 e399)))
(let ((e419 (xor e236 e172)))
(let ((e420 (ite e355 e414 e120)))
(let ((e421 (=> e208 e415)))
(let ((e422 (=> e392 e392)))
(let ((e423 (= e275 e397)))
(let ((e424 (= e419 e362)))
(let ((e425 (not e349)))
(let ((e426 (and e411 e372)))
(let ((e427 (and e398 e424)))
(let ((e428 (=> e406 e401)))
(let ((e429 (xor e423 e274)))
(let ((e430 (=> e416 e404)))
(let ((e431 (not e405)))
(let ((e432 (ite e431 e205 e418)))
(let ((e433 (not e94)))
(let ((e434 (and e429 e421)))
(let ((e435 (ite e388 e432 e425)))
(let ((e436 (ite e325 e379 e434)))
(let ((e437 (xor e371 e420)))
(let ((e438 (and e427 e433)))
(let ((e439 (xor e412 e393)))
(let ((e440 (xor e148 e436)))
(let ((e441 (or e435 e438)))
(let ((e442 (=> e114 e441)))
(let ((e443 (and e368 e408)))
(let ((e444 (not e442)))
(let ((e445 (xor e440 e426)))
(let ((e446 (=> e439 e390)))
(let ((e447 (and e437 e444)))
(let ((e448 (and e446 e443)))
(let ((e449 (and e445 e370)))
(let ((e450 (not e449)))
(let ((e451 (not e410)))
(let ((e452 (and e428 e375)))
(let ((e453 (=> e417 e451)))
(let ((e454 (xor e453 e453)))
(let ((e455 (and e452 e447)))
(let ((e456 (xor e430 e450)))
(let ((e457 (or e456 e448)))
(let ((e458 (and e457 e454)))
(let ((e459 (and e458 e373)))
(let ((e460 (=> e459 e459)))
(let ((e461 (not e460)))
(let ((e462 (and e422 e461)))
(let ((e463 (xor e455 e462)))
e463
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
